the_w:World, l:IdLnk, e:E. sends(l;e)  Msg List 

latex

Definitions	x:A. B(x), t  T, Msg, sends(l;e), S  T
Lemmas	w-onlnk wf, w-m wf, w-loc wf, w-time wf, w-Msg wf, Msg wf, w-M wf, Id wf, lsrc wf, mlnk wf, w-E wf, IdLnk wf, world wf